Inference at * 2 2 
Iof proof for Lemma decidable-filter:

.....antecedent..... NILNIL

1. T : Type
2. T List
3. u : T
4. v : T List
5. P:({x:T| (x  v)} ).
5. (xv. Dec(P(x)))  (L':T List. (L'  v & (x:T. (x  L')  ((x  v) & P(x)))))
6. P : {x:T| (x  [u / v])} 
7. x[u / v]. Dec(P(x))
  xv. Dec(P(x)) 

latex

 by (((if (((first_nat 3:n)) = 0) then (Repeat (ParallelOp ( -1))) else (RepeatFor (first_nat 3:n
 ) (ParallelOp ( -1))))) 
CollapseTHEN (((RWO "cons_member" 0) 
CollapseTHEN (MaAuto))))
C 

latex

C.

Definitions	[car / cdr], {x:A| B(x)} , xL. P(x), P & Q, a < b, Dec(P), A, f(a), L1  L2, P  Q, increasing(f;k), x(s), P  Q, P  Q, x:A. B(x), x:A  B(x), left + right, P  Q, {T}, (x  l), x:A. B(x), x:AB(x), type List, Type, t  T, , s = t
Lemmas	decidable wf, l member wf, cons member